Talk:Axiomatic system (logic)

Conjunction introduction and elimination

Am I reading this right?

A -> B -> A ^ B

I'm not seeing any mention of the branching rule used. This should be explicitly mentioned somehow. I'm assuming left branching and reading it this way: "(A implies B) implies (A and B)"

This would mean that if we accept that A implies B we have to accept B. What? And it means that if we accept that A implies B we have to accept A. What? Something seems to be wrong here.

If we assume some sort of right branching scheme it could be: "A implies (B implies (A and B))"

Which seems fine. But right branching schemes require reading all the way to the end of a potentially very long expression before you can even figure out how to group terms, and then going back to the beginning of the expression and employing the previously discovered grouping while reading the expression. Could this really be how a standard notation for a Hilbert system works? It seems to me there must be something wrong here. Perhaps the expression in question was formulated incorrectly. But either way, to avoid confusion, some convention should be employed to allow a reader to figure out notation conventions. Perhaps a section on notation should be included in each article that covers a logical system. If Wikipedia employs certain agreed upon conventions about logical notations, then one or more articles about those conventions should be crafted and those articles could be linked to in a sufficiently prominent way from articles about logical systems. Readers should not have to guess, and notation systems used should be made explicit somehow. Comiscuous (talk) 19:48, 19 December 2021 (UTC)

Archived old talk page, redid much of the article

I have archived all talk page topics that were more than five years old. I moved the article because "Hilbert system" is not what axiomatic systems in logic are always called, or even usually called, or even often. I also redid its first section, changing the part that someone made up from scratch into something that is actually supported by WP:RS, but also moving some the long, unsourced consistency and completeness proofs from Propositional calculus to here, because they are too long to go there anyway, and hopefully they can be changed into properly sourced proofs at some point. I removed the old maintenance template and added other ones to reflect the article's new range of issues.Thiagovscoelho (talk) 02:32, 2 July 2024 (UTC)

Page move from "Hilbert system" to "Axiomatic system (logic)"

An unregistered user simply undid the move, and I simply undid it back. Even if a "Hilbert system" is just one kind of axiomatic system, this article covers axiomatic systems in general, especially since I added to it. The article's sources, even before I added to it, did not support the existence of "Hilbert system" as a distinct thing. Wikipedia reflects Reliable Sources, not your personal philosophy of logic. Thiagovscoelho (talk) 21:14, 6 August 2024 (UTC)

Your article is wrong and misleading, and the undo reason essentially provided sufficient reasoning:

"A Hilbert system is just one of several kinds of axiomatic proof systems. An axiomatic system does not even have to be a formal system, and other formal proof systems are natural deduction and sequent calculus."

It is implied that an axiomatic system is something way more general, which should also become clear from reading about axioms, since they are often not stated in formal language in philosophy. But a Hilbert system is a kind of formal system.

To address your concerns, only because someone doesn't explicitly name the a type of system (which has been established for quite some time and is named after David Hilbert who laid out its foundations), it doesn't take that type away from the system. In the same way that when a cat is never explicitly addressed as an animal, it is still an animal.

In case you want to learn some basics on the topic, here is a talk also mentioning Hilbert systems and it addresses their property of how Hilbert-style proofs are similar to Collatz sequences, which makes Hilbert systems very hard to deal with in terms of computational complexity, in contrast to some other formal proof systems, such as natural deduction.

Please do not reclassify articles on the fundamentals of proof theory when you are untrained in that area, and undo your unintentional vandalism. At this point, Hilbert systems have articles in many languages, just not in English, and they're more than relevant enough to have a dedicated article. (Almost all formal axiomatic systems in literature are Hilbert systems, but your rename mistakenly suggests it would be the only way to define formal logical systems.) There was nothing in the article that was not about Hilbert systems before you moved it.

Thanks,

your fellow logician with a research focus on Hilbert systems. 134.61.98.174 (talk) 16:10, 9 August 2024 (UTC)

There seems indeed an issue with the referenced literature being too old to address Hilbert style systems by name. Looking into more recent general introductory literature on proof theory helps, for example

• S. Buss, ed. (1998) Handbook of Proof Theory. Elsevier.

as referenced under the proof theory article. But wasn't this kind of issue declared via caption in this article before you removed it? It surely didn't mean "don't fix be but move me to a whole different topic". 134.61.96.243 (talk) 16:52, 9 August 2024 (UTC)

Again, Wikipedia reflects Reliable Sources. Sure, just because something isn't supported by Reliable Sources, that doesn't mean it isn't true. But it does mean that it doesn't go on Wikipedia, at least not until the Reliable Sources catch up to covering it. If your research focus is Hilbert systems, then you should have known a lot of literature to cite about them.

This handbook you just referenced does refer to "the Hilbert style system", in pages 552–553, but it does so to refer to a very specific set of 3 rules and 15 axiom schemas, which was not what the article covered before, and is not what it covers now. (I might add it to the article later, as an example of axiomatic system.)

This other website, from Stanford University, uses the name "Hilbert System" to refer to a system of axiom schemas that is identical to the schematic form of P₂ featured in the current version of the article. (This accords with the currently cited source that attributes it to Hilbert and names it ${\mathcal {H}}$.) So it seems that the name "Hilbert system" is ambiguous and can refer to many things. If there's a clear univocal definition of "Hilbert system", then I'll make that clear in a section of this article, as well as in the Glossary of logic, as soon as I get enough references to Reliable Sources making that clear. Thiagovscoelho (talk) 18:18, 16 August 2024 (UTC)

This is ridiculous. You are cherry picking and declare most sources as non-reliable. If you just use the internet, you'll find thousands of sources talking about Hilbert systems, but you may want to check Polish and German sources as well, since this is where these terms origin from. You ignore all the arguments or you don't understand them. You clearly lack basic knowledge on the topic.

Calling something a Hilbert system merely declares the type of a proof system. When sources refer to a specific set of axioms and rules, it has nothing to do with the term "Hilbert system", which is merely about how proofs are supposed to work on its primitives.

Moreover, an axiomatic systems is still not a formal system per se. It is still false that Frege, Łukasiewicz, Russell, Whitehead and Hilbert invented axiomatic systems, those were probably rather invented by ancient Greeks.

This article is supposed to be about a specific kind of formal system (which does not mean a specific instance of a formal system), with a historical name. Acting like one would generally talk about all kinds of axiomatic systems is strongly misleading. The article is absolute garbage now from a professional standpoint. It should be moved back to Hilbert_system and reintroduce all the frequently used synonyms from the original article, i.e. "sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system", and remove the implicit false claims how all axiomatic systems would be in Hilbert style or even formalized. 2A00:8A60:C010:1:0:0:1:1026 (talk) 03:58, 18 August 2024 (UTC)

The article right now does not claim or imply that "all axiomatic systems would be in Hilbert style" or anything similar. If a "Hilbert system" is a kind of axiomatic system, then it is not the same kind in every book, since different books do not use the phrase with the same definition. Thiagovscoelho (talk) 23:54, 19 August 2024 (UTC)

False. The article currently says "an axiomatic system is a type of system of formal deduction developed by Gottlob Frege, Jan Łukasiewicz, Russell and Whitehead, and David Hilbert" which is utter bullshit. These people only developed Hilbert systems. And the article then proceeds to describe only Hilbert systems, not axiomatic systems in general.

What "Hilbert system" include is described in a lot of basic scientific literature for proof theory, as has been mentioned. For example, A. S. Troelstra, H. Schwichtenberg - Basic Proof Theory (2000, Cambridge University Press), page 51 ff.

"Then it is not the same kind in every book"

Bullshit. They are all of the same kind, obviously. That's a different thing than "they are equal". For example 1, 42, and 1337 are all numbers, i.e. all of the same kind. But they are not equal. You apparently are a mathematical crank. Please revert all your changes and do not ever edit mathematical articles again. 2A00:8A60:C010:1:0:0:1:1016 (talk) 04:31, 20 August 2024 (UTC)

If Hilbert systems are one kind of axiomatic system, then whoever develops Hilbert systems develops axiomatic systems. The sources cited in the Axiomatic_system_(logic)#Frege's_Begriffsschrift section credit Frege with developing an axiomatic system, not a "Hilbert system"; the same is true of the sources describing Łukasiewicz in Axiomatic_system_(logic)#Łukasiewicz's_P2. The source cited about Russell and Whitehead does not mention "Hilbert-style" systems either.

They are not all of the same kind, as the sources cited in the current second paragraph make clear. Your new source is just yet another different definition. Thiagovscoelho (talk) 13:29, 20 August 2024 (UTC)

Many logicians make up their own technical terms and define them for use within their own book. Sometimes multiple logicians define the same term with the same meaning, as in the case of the "Disjunctive Normal Form Theorem", which is supported by four different textbooks that used that name for that theorem. In the case of "Hilbert system", your handbook uses the name for one thing, the Stanford source I just linked uses it for a different thing, and this third source (PDF) uses the name to refer to yet a third system, one with only two axioms (plus modus ponens as an inference rule). The only thing they seem to have in common is that they are axiomatic logical systems that are vaguely attributed to David Hilbert, although without ever citing a work by Hilbert as a source. I have edited the article's lead paragraph to reflect this. Thiagovscoelho (talk) 18:37, 16 August 2024 (UTC)

So you basically admit to cherry picking. "Oh, these are logicians making up their own terms, so by my magically higher authority I hereby declare their literatur as being unreliable."

In fact, all those terms are reliable w.r.t. Wikipedia standards since they are published in scientific literature.

And they often do not cite anything by Hilbert directly since Hilbert ranges a century back and these terms have been common knowledge among logicians for more than just a few decades. Just like the foundational crisis of mathematics (here again the German article is much better) which was resolved around the 1930s, where these terms origin from.

> uses the name to refer to yet a third system, one with only two axioms

Again. The name "Hilbert system" has nothing to do with actual contents, but with how contents are arranged to form proofs. There is an infinite number of Hilbert systems. You are probably confused by terms like Euclidean space which refer to concrete objects, but the term "Hilbert system" is as abstract and general as topological space or group. 2A00:8A60:C010:1:0:0:1:1026 (talk) 04:17, 18 August 2024 (UTC)

These sources are using the name "the Hilbert system" without suggesting that there are any other ones. Some sources may support the idea that "there is an infinite number of Hilbert systems", but not all of them do. Thiagovscoelho (talk) 23:56, 19 August 2024 (UTC)

"the Hilbert system" is not a name but a description, such as "the cat (i.e. an instance of a cat that we refer to in this context)"

Of course, sources usually refer to a single instance of a Hilbert system which is precisely the one they care about. 2A00:8A60:C010:1:0:0:1:1016 (talk) 04:22, 20 August 2024 (UTC)

After some additional research on the name "Hilbert system", I have moved it from the lead paragraph to the second paragraph in order to accommodate additional information. I repeat that the literature uses the term "Hilbert system" in so many senses that it makes no sense to have an article describing them at length as if the term had a single well-known meaning; the sources cited should make this clear now. Thiagovscoelho (talk) 19:35, 16 August 2024 (UTC)

> it makes no sense to have an article describing them at length as if the term had a single well-known meaning

Umm, what? This is what Wikipedia articles are all about. There should be a dedicated article on Hilbert systems for the same reason that the articles on topological spaces and groups should remain.

Or, alternatively, for the same reasons there are corresponding Wikipedia articles in many other languages:

- German: Hilbert-Kalkül

- Polish: System Hilberta

- Czech: Hilbertovský kalkulus

- French: Système à la Hilbert

- Portuguese: Sistema de Hilbert

- Chinese: 希尔伯特演绎系统 (translates as "Hilbert deductive system")

- But English: "Axiomatic system (logic)"?

You are clearly not thinking straight. Calm down, fix your shit and we'll forget about this. Otherwise I'll request admin intervention. 2A00:8A60:C010:1:0:0:1:1026 (talk) 04:42, 18 August 2024 (UTC)

I am calm. Request admin intervention if you want to. These other language articles also lack sources; the Portuguese and Chinese ones seem to have been translated from the English one. Thiagovscoelho (talk) 23:59, 19 August 2024 (UTC)

I had added four sources to this article to support a description of the usage of the term "Hilbert system", and have added more now. You have not responded to the second paragraph of the article, but have instead made various claims about Hilbert systems in this talk page without supporting them with any sources. It is unclear what "specific kind of formal system" you think so-called Hilbert systems even are; the page, as it existed, did not differentiate it clearly from other "kinds" of axiomatic systems in logic, and, as the second paragraph now shows with citations, neither do many of the published academic Reliable Sources. Thiagovscoelho (talk) 00:01, 20 August 2024 (UTC)

I referred to plenty of valid sources by referring to plenty of articles, not only in English language about proof theory, but all those other articles in Hilbert systems in different languages. If you took any serious attempt at understanding the very basics on this topic, you would've come across some introducing literature as A. S. Troelstra, H. Schwichtenberg - Basic Proof Theory (2000, Cambridge University Press), page 51 ff. and quickly realized your erroneous ways. There were so many valid points against your changes in the comments, it seems surreal that you still believe to be in the right. You are displaying some serious mathematical crank behavior and should revert all your changes and abstain from demolishing articles that are relevant to some people that actually care about mathematical logic. 2A00:8A60:C010:1:0:0:1:1016 (talk) 04:41, 20 August 2024 (UTC)

I have added your citation to the second paragraph of the article, which you show no sign of having read yet. It cites all the sources you mentioned and many more. That is, excepting the Wikipedia articles in other languages, which are not (and do not adequately cite) WP:RS. Thiagovscoelho (talk) 12:33, 20 August 2024 (UTC)

Hi, Thiagovscoelho. Since IP has contested your WP:BOLDMOVE, do you mind starting a formal Requested Move discussion per WP:RM#CM after moving the article back to the last stable title? For transparency, I found this discussion through a help request at User talk:2A00:8A60:C010:1:0:0:1:1016 but have no opinion on the article title itself. Just thought that following the procedural solution to conflicts on article title (i.e. RM discussions) may help here. Thank you! Rotideypoc41352 (talk · contribs) 09:15, 20 August 2024 (UTC)

I am now unable to move the page back, so we have to get an admin to do this. I will create a Requested Move discussion according to the procedure, but for moving it back instead. Thiagovscoelho (talk) 12:42, 20 August 2024 (UTC)

Requested move 20 August 2024

Axiomatic system (logic) → Hilbert system – User:2A00:8A60:C010:1:0:0:1:1016 has requested that this article be moved to "Hilbert system", which was the article title before my recent substantial revisions. He believes that the current article misleads readers to think all axiomatic systems in logic are Hilbert systems. Thiagovscoelho (talk) 12:50, 20 August 2024 (UTC)

Oppose moving it to "Hilbert system", since the usage of the term "Hilbert system" is already well-covered by this article in the second paragraph, and the current article title fits the current article content. (For transparency, note that I was the one who moved it to the current title, as seen in discussion above.) The article describes axiomatic systems in logic, in general, which is what it always did. The confusion arises because, as the second paragraph of the article now makes clear (with citations), many authors use "Hilbert-style system" to describe any deduction system that has axioms (and not only inference rules), which is to say, (what most other authors call simply) an axiomatic system. (Hence, the old version of the article described a "Hilbert system", though without sources, as "a finite sequence of formulas in which each formula is either an axiom or is obtained from previous formulas by a rule of inference", which, as the sources cited in the current version of the article show, is just what any axiomatic system of logic is.) Some authors of WP:RS do define a "Hilbert system" as a specific kind of axiomatic system, but they give conflicting definitions of it, so that it's not clear which of those definitions the article should be covering if it really were specifically only about the supposed subset of axiomatic systems that can be described as "Hilbert-style" systems. User:2A00:8A60:C010:1:0:0:1:1016 claims that "there was nothing in the article that was not about Hilbert systems", in the sense of a "specific kind of formal system", before my recent revisions, but the content before those revisions was simply stated dogmatically without citing any sources, so that it could not be verified to be true only of some highly specific sense of "Hilbert systems". When pressed to give sources in this talk page, User:2A00:8A60:C010:1:0:0:1:1016 gave two academic sources with specific, but conflicting definitions of "Hilbert system" (both of which are now, at any rate, mentioned in the article), and also cited the Wikipedia articles on "Hilbert system" in different languages, all of which were at least just as lacking in sources as the previous English one (before my recent revisions), and, in brief, none of which cited any WP:RS supporting his contentions. Thiagovscoelho (talk) 12:55, 20 August 2024 (UTC)